Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    app(D,t)  → 1
2:    app(D,constant)  → 0
3:    app(D,app(app(+,x),y))  → app(app(+,app(D,x)),app(D,y))
4:    app(D,app(app(*,x),y))  → app(app(+,app(app(*,y),app(D,x))),app(app(*,x),app(D,y)))
5:    app(D,app(app(-,x),y))  → app(app(-,app(D,x)),app(D,y))
6:    app(D,app(minus,x))  → app(minus,app(D,x))
7:    app(D,app(app(div,x),y))  → app(app(-,app(app(div,app(D,x)),y)),app(app(div,app(app(*,x),app(D,y))),app(app(pow,y),2)))
8:    app(D,app(ln,x))  → app(app(div,app(D,x)),x)
9:    app(D,app(app(pow,x),y))  → app(app(+,app(app(*,app(app(*,y),app(app(pow,x),app(app(-,y),1)))),app(D,x))),app(app(*,app(app(*,app(app(pow,x),y)),app(ln,x))),app(D,y)))
There are 48 dependency pairs:
10:    APP(D,app(app(+,x),y))  → APP(app(+,app(D,x)),app(D,y))
11:    APP(D,app(app(+,x),y))  → APP(+,app(D,x))
12:    APP(D,app(app(+,x),y))  → APP(D,x)
13:    APP(D,app(app(+,x),y))  → APP(D,y)
14:    APP(D,app(app(*,x),y))  → APP(app(+,app(app(*,y),app(D,x))),app(app(*,x),app(D,y)))
15:    APP(D,app(app(*,x),y))  → APP(+,app(app(*,y),app(D,x)))
16:    APP(D,app(app(*,x),y))  → APP(app(*,y),app(D,x))
17:    APP(D,app(app(*,x),y))  → APP(*,y)
18:    APP(D,app(app(*,x),y))  → APP(D,x)
19:    APP(D,app(app(*,x),y))  → APP(app(*,x),app(D,y))
20:    APP(D,app(app(*,x),y))  → APP(D,y)
21:    APP(D,app(app(-,x),y))  → APP(app(-,app(D,x)),app(D,y))
22:    APP(D,app(app(-,x),y))  → APP(-,app(D,x))
23:    APP(D,app(app(-,x),y))  → APP(D,x)
24:    APP(D,app(app(-,x),y))  → APP(D,y)
25:    APP(D,app(minus,x))  → APP(minus,app(D,x))
26:    APP(D,app(minus,x))  → APP(D,x)
27:    APP(D,app(app(div,x),y))  → APP(app(-,app(app(div,app(D,x)),y)),app(app(div,app(app(*,x),app(D,y))),app(app(pow,y),2)))
28:    APP(D,app(app(div,x),y))  → APP(-,app(app(div,app(D,x)),y))
29:    APP(D,app(app(div,x),y))  → APP(app(div,app(D,x)),y)
30:    APP(D,app(app(div,x),y))  → APP(div,app(D,x))
31:    APP(D,app(app(div,x),y))  → APP(D,x)
32:    APP(D,app(app(div,x),y))  → APP(app(div,app(app(*,x),app(D,y))),app(app(pow,y),2))
33:    APP(D,app(app(div,x),y))  → APP(div,app(app(*,x),app(D,y)))
34:    APP(D,app(app(div,x),y))  → APP(app(*,x),app(D,y))
35:    APP(D,app(app(div,x),y))  → APP(*,x)
36:    APP(D,app(app(div,x),y))  → APP(D,y)
37:    APP(D,app(app(div,x),y))  → APP(app(pow,y),2)
38:    APP(D,app(app(div,x),y))  → APP(pow,y)
39:    APP(D,app(ln,x))  → APP(app(div,app(D,x)),x)
40:    APP(D,app(ln,x))  → APP(div,app(D,x))
41:    APP(D,app(ln,x))  → APP(D,x)
42:    APP(D,app(app(pow,x),y))  → APP(app(+,app(app(*,app(app(*,y),app(app(pow,x),app(app(-,y),1)))),app(D,x))),app(app(*,app(app(*,app(app(pow,x),y)),app(ln,x))),app(D,y)))
43:    APP(D,app(app(pow,x),y))  → APP(+,app(app(*,app(app(*,y),app(app(pow,x),app(app(-,y),1)))),app(D,x)))
44:    APP(D,app(app(pow,x),y))  → APP(app(*,app(app(*,y),app(app(pow,x),app(app(-,y),1)))),app(D,x))
45:    APP(D,app(app(pow,x),y))  → APP(*,app(app(*,y),app(app(pow,x),app(app(-,y),1))))
46:    APP(D,app(app(pow,x),y))  → APP(app(*,y),app(app(pow,x),app(app(-,y),1)))
47:    APP(D,app(app(pow,x),y))  → APP(*,y)
48:    APP(D,app(app(pow,x),y))  → APP(app(pow,x),app(app(-,y),1))
49:    APP(D,app(app(pow,x),y))  → APP(app(-,y),1)
50:    APP(D,app(app(pow,x),y))  → APP(-,y)
51:    APP(D,app(app(pow,x),y))  → APP(D,x)
52:    APP(D,app(app(pow,x),y))  → APP(app(*,app(app(*,app(app(pow,x),y)),app(ln,x))),app(D,y))
53:    APP(D,app(app(pow,x),y))  → APP(*,app(app(*,app(app(pow,x),y)),app(ln,x)))
54:    APP(D,app(app(pow,x),y))  → APP(app(*,app(app(pow,x),y)),app(ln,x))
55:    APP(D,app(app(pow,x),y))  → APP(*,app(app(pow,x),y))
56:    APP(D,app(app(pow,x),y))  → APP(ln,x)
57:    APP(D,app(app(pow,x),y))  → APP(D,y)
The approximated dependency graph contains one SCC: {12,13,18,20,23,24,26,31,36,41,51,57}. Hence the TRS is terminating.
Tyrolean Termination Tool  (1.27 seconds)   ---  May 3, 2006